Nuprl Lemma : equiv_rel_iff
13,42
postcript
pdf
EquivRel(
;
A
,
B
.
A
B
)
latex
Up
rel
1
,
rel
1
Definitions
EquivRel(
T
;
x
,
y
.
E
(
x
;
y
))
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Sym(
T
;
x
,
y
.
E
(
x
;
y
))
,
P
Q
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
P
&
Q
,
t
T
,
Lemmas
iff
wf
origin
;A,B.A 
B) ;A,B.A B) Q Q
x:A. B(x) Q
T